A:Type, eq:EqDecider(A), x, y:A, v, z:Top. x : v(y)?z ~ if eqof(eq)(x,y) v else z fi 

latex

Definitions	Top, EqDecider(T), x : v, f(x)?z, f(x), x  dom(f), T, P  Q, p  q, eqof(d), false, p  q, true, True, Unit, P  Q, , Prop, b, t  T, b, x:A. B(x), P  Q, P & Q, A, P  Q, False
Lemmas	assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, true wf, btrue wf, band wf, false wf, bool wf, bfalse wf, eqof wf, bor wf, and functionality wrt iff, assert of band, bnot thru bor, squash wf, assert of bor, deq wf, top wf